\begin{tabbing}
$\forall$$T$:(Id$\rightarrow$Type), ${\it tab}$:secret{-}table($T$), $x$:Atom1.
\\[0ex]isl(st{-}lookup(${\it tab}$;$x$))
\\[0ex]$\Rightarrow$ (\=$\exists$$n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it tab}$$\parallel$ }}$.\+
\\[0ex]$n$$\leq$ptr(${\it tab}$)
\\[0ex]\& st{-}atom(${\it tab}$;$n$) $=$ $x$
\\[0ex]\& outl(st{-}lookup(${\it tab}$;$x$)) $=$ $\langle$key(${\it tab}$;$n$)$,\,$data(${\it tab}$;$n$)$\rangle$ $\in$ ($\mathbb{N}$+Atom1)$\times$data($T$))
\-
\end{tabbing}